Sequence.select and Sequence.update now require `0 <= i < length(s)`;
Sequence.take and Sequence.drop require `0 <= n <= length(s)`. PrecondElim
picks these up and generates VC obligations at call sites, both in
statement positions (via transformStmt) and in pure positions (via
mkContractWFProc / mkFuncWFProc) — so requires/ensures/quantifier-body
subscripts are also covered.

Obligations carry the propertyType metadata "outOfBoundsAccess" (new
MetaData constant) and flow through a new PropertyType.outOfBoundsAccess
enum variant — with matching entries in the statement-eval /
obligation-extraction / cmd-eval metadata-to-PropertyType conversion
sites — to finally render as "out-of-bounds-access" in SARIF output,
matching how divisionByZero and arithmeticOverflow are classified.

Side effect: `propertyTypeToClassification` in SarifOutput.lean was
previously dead code; `vcResultToSarifResult` never set
`properties.propertyType` so the SARIF output defaulted every obligation
to "assert". Wiring this up means divisionByZero and arithmeticOverflow
obligations now also classify correctly in SARIF — a pre-existing bug
this PR incidentally fixes.

New tests in StrataTest/Transform/PrecondElim.lean:
- Test 10:  Sequence.select in a procedure body emits the bounds assert
            (PrecondElim is unconditional — it inserts regardless of any
            surrounding requires guard; the SMT solver discharges).
- Test 10c: Sequence.select inside a requires clause triggers the
            $$wf-procedure path (mkContractWFProc).
- Test 10d: Sequence.select inside a function body triggers the
            function-body $$wf path (mkFuncWFStmts).
- Test 11:  collectPrecondAsserts attaches outOfBoundsAccess metadata
            for all four partial ops and a nested call. Mirrors
            OverflowCheckTest.lean. Also verifies Sequence.length emits
            no obligation (it is total).

New property-classification tests in
StrataTest/Languages/Core/Tests/SarifOutputTests.lean cover all five
PropertyType variants, exercising the SARIF wiring fix in commit 3.

Collateral test updates for real behavioral changes:
- StrataTest/Languages/Core/Examples/Seq.lean: expected VC output
  includes the new bounds obligations (all SMT-provable from the
  surrounding context, except the pre-existing contains_yes unknown).
- StrataTest/Languages/Core/Tests/ProgramEvalTests.lean: Sequence func
  signatures now render with the attached requires clauses.

Add `seqName : String := "s"` parameter so the helper no longer hardcodes
the input variable name in a string literal three definitions away from
the call sites that depend on it. All four current callers (`Sequence.{select,update,take,drop}`) name their `Sequence a` input `"s"` and use the
default. A future partial Sequence op with a different input name need
only pass it explicitly rather than rely on the hidden literal.

Mismatches between a function's declared inputs and the names used in its
preconditions remain caught at elaboration by `polyUneval`'s `h_precond`
free-vars check; this change only reduces the code-distance between
cause and effect.

Cherry-pick target: PR #1100. The change sits inside #1100's
`mkSeqBoundsPrecond`, so it belongs there. When #1100 lands and this
branch rebases on main, the commit will be deduplicated automatically.